T:Type, R:(TT).
sum_of_torder(T;R)  (x, y, x', y':T. (R(x,y))  (R!(y',y))  ((R(x,y'))  (x = y'))) 

latex

Definitions	x:AB(x), , Type, P  Q, P  Q, left + right, s = t, R!, f(a), x:A. B(x), t  T, sum_of_torder(T;R), P & Q, x:A  B(x), {T}, A c B, A, False
Lemmas	sum of torder wf, rel-immediate wf